package kodkod.analysis;

import java.util.*;

import kodkod.analysis.*;
import kodkod.analysis.AST.ExtendedVoidVisitor;
import kodkod.analysis.AST.GraphVisitor;
import kodkod.ast.*;
import kodkod.ast.operator.*;
import kodkod.engine.fol2sat.Translation;

public class HCVisitor extends ExtendedVoidVisitor {
		
	Translation translation;
	
	boolean negated = false;
	
	static final boolean NEGATION_DOUBLE_VISIT = true;
	static final boolean SKIP_EXIST = true;
	
	public static int orDepth = 0;
	public static int qDepth = 0;
	
	public HashSet<Formula> formulas = new HashSet<Formula>();
	
	public HashSet<Expression> boundLow = new HashSet<Expression>();
	public HashMap<Formula, Integer> orDepths = new HashMap<Formula, Integer>();
	public HashMap<Formula, Integer> qDepths = new HashMap<Formula, Integer>();
	
	public HCVisitor(Translation translation) {
		this.translation = translation;
		this.visit(translation.formula);
	}
	
	@Override
	protected boolean visited(Node n) {
		return false;
	}
	
	public boolean zeros(Expression exp) {
		return boundLow.contains(exp);
	}
	
	private void register(Formula f) {
		orDepths.put(f, orDepth);
		qDepths.put(f, qDepth);
		
		formulas.add(f);
	}
	
	@Override
	public void visit(Comprehension comprehension) {
		for (Decl decl : comprehension.decls()) {
			super.visit(decl);
		}

		if (NEGATION_DOUBLE_VISIT) orDepth++;
		
		super.visit(comprehension.formula());
		
		if (NEGATION_DOUBLE_VISIT) {
			negated = !negated;
			super.visit(comprehension.formula());
			negated = !negated;
		}
		

		if (NEGATION_DOUBLE_VISIT) orDepth--;
	}
	
	public void visit(IfExpression ifExpr) {
		if (NEGATION_DOUBLE_VISIT) orDepth++;
		
		super.visit(ifExpr);
		
		if (NEGATION_DOUBLE_VISIT) {
			negated = !negated;
			super.visit(ifExpr);
			negated = !negated;
		}
		
		if (NEGATION_DOUBLE_VISIT) orDepth--;
	}
	
	public void visit(IfIntExpression intExpr) {
		if (NEGATION_DOUBLE_VISIT) orDepth++;
		
		super.visit(intExpr);
		
		if (NEGATION_DOUBLE_VISIT) {
			negated = !negated;
			super.visit(intExpr);
			negated = !negated;
		}
		
		if (NEGATION_DOUBLE_VISIT) orDepth--;
	}

	@Override
	public void visit(IntComparisonFormula intComp) {
		if (!(negated && intComp.op().equals(IntCompOperator.EQ))) {
			IntCompOperator op = intComp.op();
			
			boolean leftBoundLow = false;
			boolean rightBoundLow = false;
			
			if (op.equals(IntCompOperator.LT) || op.equals(IntCompOperator.LTE)) {
				if (!GraphVisitor.negated) leftBoundLow = true;
				else rightBoundLow = true;
			}
			if (op.equals(IntCompOperator.GT) || op.equals(IntCompOperator.GTE)) {
				if (!GraphVisitor.negated) rightBoundLow = true;
				else leftBoundLow = true;
			}
			
			Casts pLeft = new Casts(intComp.left());
			Casts pRight = new Casts(intComp.right());
			
			if (pRight.size() == 0 || pLeft.size() == 0) {//constant bound
				if (leftBoundLow) {
					for (Expression cast : pLeft) {
						boundLow.add(cast);
					}
				} else if (rightBoundLow) {
					for (Expression cast : pRight) {
						boundLow.add(cast);
					}
				}
				register(intComp);
			}
		}		
		
		super.visit(intComp);
	}

	@Override
	public void visit(QuantifiedFormula qFormula) {
		if (negated != qFormula.quantifier().equals(Quantifier.ALL)) {
			for (Decl decl : qFormula.decls()) {
				Analyzer.allDecls.put(decl.variable(), decl.expression());
			}
		}
		
		int expressionSize = 0;
		for (Decl decl : qFormula.decls()) {
			expressionSize += BoundsExtension.get(decl.variable()).size();
		}
		
		qDepth += qFormula.decls().size();
		
		register(qFormula);
		if (!SKIP_EXIST || negated != qFormula.quantifier().equals(Quantifier.ALL)) {
			super.visit(qFormula);
		}
		
		qDepth -= qFormula.decls().size();
	}
	
	@Override
	public void visit(NaryFormula node) {
		if (negated == node.op().equals(FormulaOperator.AND)) {
			orDepth += node.size()-1;
			for(Formula child : node) {
				child.accept(this);
			}
			orDepth -= node.size()-1;
		} else {
			super.visit(node);
		}
	}

	@Override
	public void visit(BinaryFormula node) {
		if ((negated && node.op().equals(FormulaOperator.AND)) || (!negated && node.op().equals(FormulaOperator.OR))) {
			orDepth++;
			node.left().accept(this);
			node.left().accept(this);
			orDepth--;
		} else if (node.op().equals(FormulaOperator.IMPLIES)) {
			orDepth++;
			negated = !negated;
			node.left().accept(this);
			negated = !negated;
			node.right().accept(this);
			orDepth--;
		} else {
			if (NEGATION_DOUBLE_VISIT) orDepth++;
			super.visit(node);
			if (NEGATION_DOUBLE_VISIT) {
				negated = !negated;
				super.visit(node);
				negated = !negated;
			}
			if (NEGATION_DOUBLE_VISIT) orDepth--;
		}
	}

	@Override
	public void visit(NotFormula not) {
		negated = !negated;
		super.visit(not);
		negated = !negated;
	}

	@Override
	public void visit(ComparisonFormula compFormula) {
		if (compFormula.left() == compFormula.right()) return;
		if (compFormula.left() instanceof Variable && compFormula.right() instanceof Variable) {
			Expression left = Analyzer.decls.get(compFormula.left());
			Expression right = Analyzer.decls.get(compFormula.right());
			if (left != null && left == right) return;
		}
		
		if (!negated) register(compFormula);
		
		super.visit(compFormula);
	}

	@Override
	public void visit(MultiplicityFormula multFormula) {
		if (negated == multFormula.multiplicity().equals(Multiplicity.SOME)) {
			boundLow.add(multFormula.expression());
			register(multFormula);
		}
		
		super.visit(multFormula);
	}
}
